% \setcounter{secnumdepth}{-1}

\chapter*{Abstract}

The work presented in this report is focussed on the design and development of the \K Framework ~\cite{rosu-serbanuta-2010-jlap} such that it offers support for symbolic execution. There are many symbolic execution frameworks but all of them are specialized on a specific language. The advantages of introducing symbolic execution support to \K are the following: \K would become the first general purpose symbolic execution framework, there would be a clear distinction between language independent and language specific aspects of symbolic execution, and the symbolic execution  in \K would be the first based on the operational formal semantics of a programming language.

This is the first report on this research and its main purpose is to describe the steps which must be done such that it can be finished on time and we can get new and strong results. The report contains the research description, a detailed progress report which includes the main activities started and finished, a technical and a more informal description of the results, the published papers, and a plan containing future works.


% \setcounter{secnumdepth}{-1}
\chapter{Research description}

\section{Overview of the Main Goals}
\label{rd:ov}

The initial goal of this research was to develop the \K semantics of a core of OCL (Object Constraint Language) according to OMG standard, version 2.3. The purpose was to define both the static parts of OCL (corresponding to well-formedness constraints and queries over UML models) and the dynamic parts (corresponding to pre/post conditions of methods). The dynamic part of OCL involves symbolic execution of methods using OCL annotations given as pre/post conditions. The results obtained when developing symbolic execution encouraged the idea of designing a generic symbolic execution framework for languages using \K. So, the central aims of this research are the following:
\begin{itemize}
\item {\it Support for symbolic execution in \K framework}. This involves adding symbolic values to existent \K builtins and creating a mechanism for generating such values. Also, we need to offer the user the possibility to define its own symbolic values which may consist in symbolic pieces of programs. The support for symbolic execution must be provided together with its own well-defined theoretical background.
\item {\it Applications of symbolic execution}. Since the symbolic execution is meant to be general, we need to create a range of applications in order to prove that the support we offer is generic. This goal is linked with the first one in the sense that most of the development of the support itself is driven by creating applications which use symbolic execution. This allows to find a clear distinction between language independent and language specific aspects of symbolic execution. A subgoal would be to redefine the dynamic part of OCL using the new approach and to test it on modeling languages.
\item {\it Implementing deductive systems over \K symbolic executions}. This goal consists in implementing existent deductive systems (e.g. Reachability Logic) together with specific theories depending on the application needs (e.g. heap, cache, arrays, ...). The result of this work should allow users to choose an existent deductive system to be applied or to define their own deductive system.

\end{itemize}




% \setcounter{secnumdepth}{-1}
\chapter{Progress report}

\section{Proposed approach}

As already stated in the previous section the main goal of the research is to add support for symbolic execution to the \K framework and support for applying deductive systems on top of that. In order to achieve this goal, we established some general steps to follow which are listed below:
\begin{itemize}
\item Investigate the architecture of \K framework, in order to be able to add support for symbolic execution into it. Also, provide some formal background for symbolic execution such that it extends the existent \K formalism.
\item Investigate some applications of symbolic execution by extracting the common aspects which should be offered as support by \K and also isolate the language or domain specific aspects related to symbolic execution.
\item Investigate the most recent work done on deductive systems and design a way to integrate them into \K as well.
\end{itemize}

The steps described above are very general but cover the whole subject of this research. Each such step is split into specific well-defined activities which are discussed in sections below.



\section{Main achievements}
The main activities done in the first year were related to reading documentation and learning \K framework. The following tasks are completed or almost finished, and are highly relevant to the current work:
\begin{itemize}
\item Adapt the existent OCL semantics to the most recent version of the \K framework.
\item Design and implement in \K a parser for OCL. Note that OCL was using an external parser.
\item Extend OCL syntax and semantics to accept pre/post conditions on methods.
\item Executing methods using symbolic execution of pre/post conditions.
\item Identifying parts of the symbolic execution which may have been provided by the \K framework: symbolic values for integers and Booleans and a mechanism for generating such values. 
\item Adding symbolic values as builtins in \K and creating a pattern for symbolic values generation using cells.
\item Investigate and create a simple application on the top of the \K semantics of IMP (a simple imperative language which contains assignments, if-statements and while-loops) which consists in creating a program which uses symbolic values and the result is a first order logic formula.
\item Creating a connection from an existing SMT solver to \K such that we can verify the satisfiability of formulas obtained when executing symbolically IMP programs. Since \K uses Maude for execution, we had to recompile Maude in order to be able to use its builtin model-checker (search command).
\end{itemize}
The steps above allowed us to verify that adding symbolic execution support in \K framework is feasible and we obtained some promising results. For instance, we enriched the syntax of IMP with assertions and we were able to verify them using the connection to the solver. Additionally, for a wrong IMP program which is supposed to find minimum among three given variables we can model-check it and find all the executions and the result of the assertion which states that minimum is less or equal than any other variable.
We also worked on the formal background of the symbolic execution enriching the existing \K formalism. We identified the concrete and symbolic transition systems determined by concrete and symbolic execution. We are working now on proving that there exists a strong bisimulation between the two transition systems.



\section{Research papers and publications}

The research done until now also produced some interesting results which ended up as publications in different workshops/conferences:
\begin{itemize}
\item The extended \K semantics of OCL has been submitted for publication as a regular paper entitled "Towards a K Semantics for OCL" in the post-proceedings of the \K'11 workshop, held at Cheile Gr{\u a}di{\c s}tei, Bra{\c s}ov, Rom{\^ a}nia.
\item In order to execute real programs \K framework offers a tool called {\tt krun} which is able to execute programs using directly the \K semantics of a programming language. A limitation of it was that it was not able to deal real input/output operations. We added this feature directly to Maude and we published the paper "Making Maude Definitions more Interactive" in the post-proceedings of WRLA'12(Workshop on Rewriting Logic and Applications), held in Tallinn, Estonia.
\item Improving implementation of the \K framework, changing the syntax of the \K language, adding program execution features, and finishing the \K semantics of made the framework evolve to a stable release. We published the paper "Executing Formal Semantics with the K Tool" in the proceedings of the 18th International Symposium on Formal Methods (FM'12), held in Paris, France. Related to the stable release of \K framework, we also submitted "The K Primer (version 2.5)" for publishing in \K'11 post-proceedings.

\item A more technical paper is "Automating Abstract Syntax Tree construction for Context Free Grammars", which aims to automatize the construction of \K specific abstract syntax trees directly from the context free grammar of a language. It was submitted and accepted for publication in post-proceeding of SYNASC 2012, published by Conference Publishing Service (CPS). The paper will be presented at Timi{\c s}oara, Rom{\^ a}nia, on 28$^{th}$ of September, 2012.
\end{itemize}



% \setcounter{secnumdepth}{-1}
\chapter{Technical report}

\section{Introduction}

Program analysis is a process consisting in automatically analyzing the behavior of computer programs. The are two main approaches: static analysis, which is performed analyzing the source code without actually running the program, and dynamic analysis which involves execution of the program on a virtual processor.\\
Symbolic execution is a well-known program analysis technique introduced three decades ago as being useful for running, testing  and debugging programs. It mainly consists in sending symbolic values as input for programs instead of concrete ones and the execution is done by manipulating program expressions involving the symbolic values. The main advantage of using symbolic execution is that it allows reasoning about multiple concrete executions of a program. On the other hand, the main disadvantage of this technique is the state space explosion determined by decision statements and loops in programs. Recently, the technique has found renewed interest in the research community due to the progress in decision procedures, new algorithmic developments and availability of powerful computers. Nowadays, the applications of symbolic execution range from automated test input generation to proving program partial correctness.

In the past years researchers spend a lot of time and energy in developing formal semantics for programming languages. The semantics of a programming language describes the meaning of the syntactical constructs of the language, showing the computation involved. There are many approaches and variations to formal semantics which can be classified as follows: denotational semantics, operational semantics and axiomatic semantics. Denotational semantics maps each language construct to a mathematical object which already has a well-defined semantics. Axiomatic semantics consists in describing some logical axioms and then apply them. Hoare logic is the canonical example of axiomatic semantics. Operational semantics involves creating an interpreter using a language which is a generally mathematical formalism. An example of such a language is \K which comes together with an entire framework for defining operational semantics for programming languages. Beside small didactic languages which explore a whole range of programming paradigms, there also several important languages  defined in \K: Verilog, Java 1.4, Scheme and C. The formal semantics of the C programming language written in \K is based on the ISO/IEC C11 standard and it is the most complete formal definition of this language.


The rest of this technical report contains a detailed description which may need additional requirements for the reader. It assumes that the reader has advanced knowledge about the \K framework and basic knowledge regarding symbolic execution.\\
Since symbolic execution is a program analysis technique which represents program inputs with symbolic values instead of actual data, we decided to add support for these values in the \K framework. To be more specific, the \K builtin types/sorts have been enriched with symbolic values without affecting the existent definitions. In most of the cases, the use of symbolic values implies symbolic calculus. To facilitate this, we integrated a specialized tool (a SMT solver) in the \K Framework and we also provide the automatic translation of primitive expressions to SMTLIB language. Section~\ref{state} contains an overview of the symbolic execution in general and its applications. In Section \ref{sec:extend} we describe the addition of symbolic values to \K. Section \ref{sec:smt} contains a detailed description of the connection to the SMT solver and a case study is shown in Section \ref{sec:example}.

\section{State of the art}

\label{state}

In 1976, James C. King describes in \cite{DBLP:journals/cacm/King76} for the first time the symbolic execution of programs. According to the authors, symbolic execution is seen as a normal execution of programs except that values are symbolic formulas over the input symbols. The paper focuses on the importance of symbolic execution in automated test generation, but it also highlights the key concepts of this analysis technique.

The use of symbolic execution in test case generation is highly motivated by the fact that programs are executed for sets of classes of inputs instead of sets of inputs. To be more explicit, testing is done by passing a set of values as input to a specific program. Unlike verification, testing gives the guarantee that for those specific inputs the program behaves correctly. What about the other possible inputs? For instance, a very simple program which gets as input only an integer can have an infinite number of inputs. A possible answer would be to test entire classes of inputs, a class representing a wider range of inputs determined by the control flow of the program. This can be achieved easily using symbolic execution by encoding program inputs as symbolic values. If the program control flow depends on input variables then case analysis is required. Otherwise, an ordinary symbolic execution is sufficient to explore all possible executions of the program. However, the input classes tested using symbolic execution are the ones determined by the inputs involved in the control flow only. This implies that symbolic execution, in the sense discussed above, remains a testing methodology, but it definitely provides better results than normal testing.

There are a few basic notions introduced in \cite{DBLP:journals/cacm/King76} related to symbolic execution. {\it Symbolic values} are substitutes for concrete values, e.g. integers. Let us consider that $\alpha$ is an integer symbolic value. The value of $\alpha$ can be any integer, but it is not known which one. For this reason, $\alpha$ can be considered and it will be used as an integer constant. When such values are provided as inputs to programs the execution semantics of the program is changed into {\it symbolic execution semantics}. The symbolic execution of regular assignments is quite natural: the expression on the right hand side is evaluated and the result is assigned to the variable. For instance, if {\tt a} and {\tt b} are two variables, where {\tt b = $\alpha$} and {\tt a = b + 1}, then the evaluation of the second assignment will attach to {\tt a} the value {\tt $\alpha$ + 1}.\\
The ``state'' of a symbolic program execution usually contains the current statement, symbolic values of program variables, the program counter and the {\it path condition}. The states are connected through edges which represent the transition from one state to another. When the control flow of a program depends on symbolic values, say an if-statement, then there are more possible choices, one for each branch. In this way, the symbolic execution determines a symbolic execution tree, where the states are the nodes and the transitions are edges. A {\it path condition} corresponds to branch of the symbolic execution tree and it has the property that it determines a unique control flow path from the program. A path condition ({\it pc}) has the initial value set to ``true'' and it is constructed when executing the program by collecting branch conditions ({\it q}): {\it pc = pc $\wedge$ q} and {\it pc = pc $\wedge$ $\lnot$q}. There are two interesting properties that path conditions can have:

\begin{itemize}
\item {\it pc} can never become identically ``false'' because there does exist a concrete input to the program which, when executed normally, will trace the same path. 
\item If {\it pc$_1$} and {\it pc$_2$} are two path conditions then $\lnot(${\it pc$_1$} $\wedge$ {\it pc$_2)$}. If {\it pc$_1$} and {\it pc$_2$} have a common part then, there exists, by construction, a state which caused the two paths to be split by adding {\it q} and {\it $\lnot$q} to the common part of the two paths. 
\end{itemize}
An important property of the symbolic execution is that if all symbolic values are instantiated by concrete values then the result is exactly the same as the one obtained when executing the program with the same concrete values.

Even if the notions above are quite common, there are lots of tools today which offer symbolic execution for specific programming languages. Java PathFinder ~\cite{DBLP:conf/kbse/2010, DBLP:conf/kbse/PasareanuR10} is a complex symbolic execution tool which uses a model checker to explore different symbolic execution paths. The approach is applied to Java programs and it can handle recursive input data structures , arrays, preconditions, and multithreading. Java PathFinder can access through an interface different SMT solvers and the user can also choose between multiple decision procedures. Other tools, like PEX~\cite{pex}, treat the input structures completely symbolically and therefore require a decision procedure to solve the resulting constraints. \\
There are some modern challenges of symbolic execution which are related mostly to library classes and native code. Such code needs an explicit modeling to make symbolic execution possible. One approach, which is meant to trick the explicit modeling by avoiding it, is combining concrete and symbolic execution, also known as {\it concolic} execution. This type of hybrid analysis, which performs both concrete and symbolic execution has been implemented by several tools in order to get dynamic test generation: DART~\cite{Godefroid:2005:DDA:1065010.1065036,Godefroid:2005:DDA:1064978.1065036}, CUTE~\cite{Sen:2005:CCU:1081706.1081750,Sen:2005:CCU:1095430.1081750}, EXE~\cite{Cadar06exe:automatically}, PEX~\cite{pex}. The main point of concolic execution is to perform concrete and symbolic execution together which outputs inputs to cover the ``new'' behavior. There are also some variations of concolic execution. One of them proposes to do first symbolic execution and then perform the concrete execution. The reason is that the symbolic execution will first detect imprecisely inputs which produce errors and the concrete execution will filter the initial results.

Another important issue of symbolic execution is scaling. The development of symbolic execution tools imposes some restrictions regarding the running time when performing symbolic execution. Therefore, some interesting techniques were developed in order to reduce the large data domains which are more amenable for verification. {\it Abstraction} is a general technique which covers a class of reduction space techniques. There are two well-known approaches: {\it over-approximations} of programs behaviors which are very useful for proving program properties (e.g. if a property is true for in an abstracted program then it remains true in the original program), and {\it under-approximation} which, unlike  over-approximations, is meant falsify properties. The other forms of abstractions are based on the ones explained above. Subsumption is used to detect already explored program paths such that, in the future that path will never be revisited. This method can be very useful for model-checking based symbolic execution frameworks. Another scaling technique is path merging: it involves the notion of path ``merging'' points, or program points where symbolic paths intersect. The merging is done by performing a logical disjunction on the symbolic states that reach a merging point.

Symbolic execution has been used initially in automated test generation. The main goal of testing is to achieve large code coverage, meaning the exploration of each statement and code branches. For this reason, symbolic execution fits well, since it is driven by the control flow of a program. Since then, many applications of symbolic execution have been explored. Below is a list of them ~\cite{DBLP:journals/sttt/PasareanuV09}:
\begin{itemize}
\item {\it Test sequence generation}. It consists in generating all sequences code which explore different symbolic paths. For instance, to test a specific method say {\tt add()} of class {\tt BinaryTree} a possible sequence could be {\tt add(1); add(1);}. This sequence will test the addition of the same value twice in a binary tree. Unfortunately, the sequence generation can be done by analyzing all combinations of method calls which is quite expensive. 
\item {\it Proving program properties}. We stated in the beginning of this section that symbolic execution is a testing methodology. It becomes useful for proving program correctness only when there is an upper bound for the number executions of each loop. Otherwise, loops must be annotated with invariants. There are several tools (e.g. Smallfoot~\cite{DBLP:conf/aplas/BerdineCO05,DBLP:conf/aplas/2005}) which use symbolic execution together with separation logic to prove Hoare triples.
\item {\it Static detection of runtime errors}. The main idea of static detection of runtime errors is to do symbolic execution on a program until a state is reached where an error occurs: null-pointer dereference, division by zero, etc. 
\item {\it Predictive testing} attempts to predict errors from correct traces.
\item {\it Invariant inference} is meant to find the most ``likely'' loop invariants.
\item {\it Program and Data Structure Repair}.
\item {\it Parallel numerical program analysis} which involves both model-checking and symbolic execution to establish the equivalence between a sequential and a parallel program.
\item {\it Differential symbolic execution} computes the logical differences between two versions of a program.
\end{itemize}



\section{Extending \K with symbolic expressions}
\label{sec:extend}

There is a very simple way of extending the existing \K builtin sorts with a value by adding a production of the form {\tt syntax Sort ::= "symval"} in the syntax definition. This declaration extends sort {\tt Sort} with the value {\tt symval} which can stand for a symbolic value. Since in practice we will probably want to assign to different variables different symbolic values we need a mechanism which will provide as much symbolic values as we want. Therefore, we define a new constructor which depends on integers. For instance, the definition of Boolean symbolic values is:

{\tt syntax BoolSymbolic ::= "symBool" "(" Int ")"}

Values {\tt symBool(0)}, {\tt symBool(1)}, and {\tt symBool(7)} are all boolean symbolic values of sort {\tt BoolSymbolic}. Actually, to link these values to \K built-in Booleans we have to add:

{\tt syntax Bool ::= BoolSymbolic}

The motivation of not adding the production {\tt "symBool" "(" Int ")"} directly to sort {\tt Bool} is that we want to be as general as possible and we want to let the users the freedom to match  on variables of sort {\tt BoolSymbolic}.

\section{Connection to SMT solver}
\label{sec:smt}
All \K modules are transformed into Maude rewrite theories and programs are executed using Maude's rewrite engine. \K built-in types are declared as sorts in Maude and their corresponding operations are hooked to Maude (already defined) internal operations for built-in sorts. To be consistent with the rest of the implementation we had to create a Maude hook to call an external SMT solver. The advantage of creating hooks instead of calling the SMT directly from \K is that we can still use the Maude model checker, because all the \K statements have a correspondent in Maude. 
The Maude operation we created for accessing the SMT solver is:\\

\begin{minipage}{\linewidth}
\centering
\hspace{-6cm}{\tt op $\#$smtCall\_ : \#String -> \#String}\\
\hspace{-4cm}{\tt [special (id-hook StringOpSymbol (smt)}\\
{\tt op-hook stringSymbol (<Strings> : ~> \#String))] .}\\
\end{minipage}\\\\
This operation gets a string which is actually SMTLIB code which usually contains constants declarations corresponding to symbolic values and an assertion representing a formula which contains Booleans and integers. The result of the operation is also a string. Using strings to communicate with the solver produces an overhead when translating the \K terms into SMTLIB and parsing the result returned by the solver. On the other hand it gives us a high degree of flexibility because in the future if we want to send more complex things to the solver all we have to do is to modify/enrich the translation into SMTLIB from \K code and also to improve the parser for the solver output. In the current implementation we provide a translator for \K's builtin Boolean expressions which can contain integers into SMTLIB. It can be accessed by the user through a \K interface: \\

\begin{minipage}{\linewidth}
\centering
\hspace{-10.5cm}{\tt // hook to \#smtCall}\\
\hspace{-3cm}{\tt syntax String ::= "smtCall" "(" String ")" [function,}\\
\hspace{9cm}{hook(\#SMT:\#smtCall\_)]}\\
\hspace{-8.4cm}{\tt syntax SmtResponse ::= "sat"}\\
\hspace{-3.3cm}{\tt      | "unsat"}\\
\hspace{-2.9cm}{\tt | "unknown"}\\
\hspace{-0.7cm}{\tt | "model" "(" Map ")"}\\

\hspace{-2.1cm}{\tt syntax SmtResponse ::= "checkSat" "(" Bool ")" [function]}\\
\hspace{2.5cm}{\tt | "getModel" "(" Bool ")" [function]}\\
\end{minipage}\\\\
The {\tt smtCall} operation is the \K correspondent of Maude's {\tt \#smtCall} operation. Sort {\tt SmtResponse} is a representation of the SMT solver output which contains satisfiability values like {\tt sat}, {\tt unsat}, {\tt unknown} or a model satisfying a specific assertion. Functions {\tt checkSat} and {\tt getModel} are implemented using {\tt smtCall}. Their arguments, Boolean expressions, are translated into SMTLIB code, sent to {\tt smtCall} and the string output returned by the SMT call is then parsed and a term of sort {\tt SmtResponse} is created.
This interface has been tested on IMP and right now {\tt checkSat} works very well including model-checking. Unfortunately, the implementation of {\tt getModel} is still in progress since it only works without model-checking.

\section{Simple example of symbolic execution}
\label{sec:example}
Let us consider the IMP program shown in Figure ~\ref{fg:minimum}. It describes a very simple algorithm which is meant to find the minimum of three numbers represented by variables {\tt a}, {\tt b}, and {\tt c}. Variable {\tt min} is supposed to hold the minimum value after the execution. As we can easily observe, the algorithm is intentionally built to return an incorrect solution on a branch: when {\tt a} $\leq$ {\tt b} and {\tt a} $>$ {\tt c} then {\tt min} becomes {\tt b} instead of becoming {\tt c}, which is commented in the algorithm.

\begin{figure}[b]
\hspace{4cm}\begin{minipage}{.2\linewidth}
\ttfamily
\selectfont
\begin{tabular}[t]{l l l}
var a, b, c, min;&&\\
if ( a <= b )&&\\
&\hspace{-8.5cm}then if (a <= c)&\\
&&\hspace{-7.5cm}then min := a\\
&&\hspace{-7.5cm}else min := b\\
&&\hspace{-7.5cm}// else min := c\\
&\hspace{-8.5cm}else if (b <= c)&\\
&&\hspace{-7.5cm}then min := b\\
&&\hspace{-7.5cm}else min := c;\\
assert(min <= a and min <= b and min <= c)&&\\
\end{tabular}
\end{minipage}
\caption{IMP program for finding minimum of three numbers}
\label{fg:minimum}
\end{figure}

When executing symbolically the program from Figure ~\ref{fg:minimum}, each input variable is assigned with a symbolic value: {\tt a := symInt(a)}, {\tt b := symInt(b)}, and {\tt c := symInt(c)}. After assignments, the main {\tt if} statement has to be executed. At this point, there two possible choices: {\tt symInt(a)} $\leq$ {\tt symInt(b)} or {\tt symInt(a)} $>$ {\tt symInt(b)}. Maude will choose randomly one of these program paths determined by the {\tt if} statement. To keep track of which one was chosen we can store extra-information by collecting the conditions from the {\tt if} statements. A possible execution can return the following condition:\\

\begin{minipage}{\linewidth}
\ttfamily
\selectfont
\hspace{-0.7cm}symInt(a) $\leq$ symInt(b) $\wedge$ symInt(a) > symInt(c) $\wedge$ symInt(b) > symInt(a)\\
\end{minipage}

Obviously, this first order logic formulae above is false because the first and the last terms of the conjunction are contradictory. When running the Maude model-checker ({\tt search}) we get all possible behaviors:\\

\begin{minipage}{\linewidth}
\ttfamily
\fontsize{10}{12}
\selectfont
\hspace{-0.7cm}
\begin{tabular}{ l || r }
\hline \hline
symInt(a) $\leq$ symInt(b) $\wedge$ symInt(a) $\leq$ symInt(c) & true \\
\hline
symInt(a) $>$ symInt(b) $\wedge$ symInt(b) $\leq$ symInt(c) & true \\
\hline
symInt(a) $>$ symInt(b) $\wedge$ symInt(b) > symInt(c) & true \\
\hline
symInt(a) $\leq$ symInt(b) $\wedge$ symInt(a) > symInt(c) $\wedge$ symInt(b) $\leq$ symInt(a) & false \\
\hline
symInt(a) $\leq$ symInt(b) $\wedge$ symInt(a) > symInt(c) $\wedge$ symInt(b) > symInt(a) & false \\
\hline \hline
\end{tabular}\\\\
\end{minipage}

The table above contains in the left column all formulas determined by the symbolic execution of the IMP program shown in Figure~\ref{fg:minimum} and in the right column the corresponding value of the {\tt assert} statement. Analyzing a bit each formula we can figure out the path considered for execution and we can find if this path makes the assertion false. In our case, the assertion is false when the condition of the first {\tt if} statement is true ({\tt symInt(a)} $\leq$ {\tt symInt(b)}) and the inner {\tt if} on {\tt then} branch is false ({\tt symInt(a)} $>$ {\tt symInt(c)}).
This simple application of symbolic calculus is able to find the paths of a program which violate a certain property. 




% \setcounter{secnumdepth}{-1}
\chapter{Future work}

As already stated in the previous sections we developed the basic support for symbolic calculus in \K. We created some applications (e.g. OCL pre/post conditions, symbolic execution of IMP programs) and we obtained quite interesting results. The research itself was from the beginning oriented to technical issues but the results obtained gave us relevant ideas of how to design and implement the support for symbolic execution and also helped us to understand how to develop a corresponding formalism.\\
The short term objective of this research is to improve the symbolic calculus support by investigating more examples and applications of symbolic execution. We only support now integers and Booleans as symbolic values and a connection with an SMT solver which is able to deal with formulas involving symbolic values. Real-life languages may need support for other types (e.g. floats) or users would want to have symbolic values representing their own data structures. Together with this, the main objective for the second year will include also the formal background for symbolic execution integrated in the existent \K framework formalism.
To summarize, below is the list of future tasks:
\begin{enumerate}
\item {\it Implementation issues} .
This task includes the continuous development of the tool so it is going to be spread on the entire period of this research. There are some tasks which must be done as soon as possible (1 month):
\begin{enumerate}
\item Finish the implementation of {\tt getModel}
\item Add symbolic values for the rest of the builtin sorts (e.g. floats)
\end{enumerate}
\item {\it Formalization of symbolic execution in \K}. 
The estimated time for achieving this task is less than a half of year. The task has already started and the only things left are the proofs.
\item {\it Applications of symbolic execution in real languages}. 
This research was driven so far by the IMP programming language and OCL constraints language. Real life programming language may raise different issues or requirements from symbolic execution, so we want to take advantage of the (under development) \K semantics of the Java programming language. As a preliminary approach, we will start with simple symbolic execution of programs like we did for IMP and then we will try to figure out how to express properties about symbolic objects. The best time approximation we can give is six months, but if the results are promising we will continue the work on this topic.

\item {\it Investigation of Reachability Logic deductive system}. This task is more like a long term task which involves more documentation. Its purpose is to implement a deductive system which can be used as a generic feature, but this asks for more study regarding the requirements of the deductive system and the symbolic execution we provide. The estimated period of time for this task is probably six to eight months and it will start in the last quarter of the second year of research.
\end{enumerate}


This report contains roughly the thesis which will drive the dissertation based on this research. Regarding the content of the report, it contains both complete and clear ideas about tasks/results and incomplete descriptions of different steps. Even so, we stated the aims of the thesis in quite clear statements, only details remaining underspecified. To conclude, this report contains a detailed description of the research domain, the major aims of this research together with the main achievements of the first year of work and a plan for the remaining phase of the research.
